package base;

/**
 * Created by IntelliJ IDEA. User: njussien Date: 30/11/12 Time: 10:40
 */
public class PourTout extends Quantification {

	// ///////////////
	// CONSTRUCTOR //
	// ///////////////

	public PourTout(Variable x, Formule f) {
		super(x, f);
	}

	// ///////////
	// METHODS //
	// ///////////

	@Override
	public Formule negation() {
		return new Existe(x, new Non(f));
	}

	@Override
	public Formule descendreNon() {
		return new PourTout(x, f.descendreNon());
	}

	@Override
	public Formule enleveEquImp() {
		return new PourTout(x, f.enleveEquImp());
	}

	public void substituer(Variable var, Terme terme) {
		if (var.getName().equals(x.getName())) {
			x = var;
		}
		f.substituer(var, terme);
	}

	@Override
	public Formule remonterQuantificateurs() {
		return new PourTout(x, f.remonterQuantificateurs());

	}

	@Override
	public Formule toConjonctive() {
		return new PourTout(x, f.toConjonctive());
	}

	public String toString() {
		return "Pour tout " + x.toString() + " " + f.toString();
	}

	@Override
	public Formule copy() {
		return new PourTout(x.copy(), f.copy());
	}
}
